(declare-fun a () Real)
(declare-fun mWoMy_new () Real)
(declare-fun d () Real)
(declare-fun af () Real)
(declare-fun ag () Real)
(declare-fun j () Real)
(declare-fun b () Real)
(declare-fun ah () Real)
(declare-fun c () Real)
(declare-fun aj () Real)
(declare-fun ai () Real)
(declare-fun e () Real)
(declare-fun aa () Real)
(declare-fun ctphm_new () Real)
(declare-fun g () Real)
(declare-fun h () Real)
(declare-fun i () Real)
(declare-fun k () Real)
(declare-fun l () Real)
(declare-fun m () Real)
(declare-fun n () Real)
(declare-fun o () Real)
(declare-fun p () Real)
(declare-fun q () Real)
(declare-fun r () Real)
(declare-fun s () Real)
(declare-fun t () Real)
(declare-fun u () Real)
(declare-fun ep () Real)
(declare-fun v () Real)
(declare-fun w () Real)
(declare-fun x () Real)
(declare-fun y () Real)
(declare-fun z () Real)
(declare-fun ab () Real)
(declare-fun ak () Real)
(declare-fun ac () Real)
(declare-fun ad () Real)
(declare-fun ae () Real)
(assert (not (exists ((o Real)) (or (and (or (and (or (and (or (and (distinct (- d) d) (= (- ai w) 0.0 (- b (- ah o))) (distinct (/ 7 b (+ 27 ah o)) 2.0) (= p 2.0)) (>= (+ s (* 0 (* 2.0 (- (- 1 aj r))))) 0) (distinct q 2.0)) (< 0 r ag)) (> 0.0 h)) (<= h u)) (<= 0.0 l) (> l u)) (>= 0.0 (* af (- j l))) (<= 0.0 u)) (< 0.0 ep) (and (= (* e x) (- g ac)) (> 0.0 (- mWoMy_new (- j))) (=> (=> (or (<= 0.0 o) (<= o (- mWoMy_new (* 9 j l)))) (and (<= (- ai w) u) (<= 0.0 (+ (* (+ 41 af) o) m)) (>= (+ (* (- af (/ 76 j l)) o) m) u) (<= (+ o 0.0) ep))) (= c 2.0)))))))
(assert (not (exists ((f Real)) (=> (and (or (and (or (and (=> (<= 0.0 (- ctphm_new ep)) (<= (- 5 ctphm_new ep) 0) (or (and (<= 0.0 (+ (* (* (* 6 1.0) ak) (- 255 ctphm_new ep)) (- aa u))) (<= (+ (* (* 4 ak) (+ 11 ctphm_new ep)) 0) y)) (< ctphm_new ad))) (<= 0.0 (- a h))) (<= 0.0 (- aa u))) (>= (- aa u) y))) (<= 0.0 (- 8 b n)) (<= n y (+ 9 mWoMy_new i)) (< 0.0 y) (< 0.0 ad)) (or (= ae 2.0) (<= (/ 91 (* (- (- 1.0) ak) (- a h)) (- aa u)) y))))))
(assert (= a (+ h ac)))
(assert (= mWoMy_new (* i z)))
(assert (= af (+ k z)))
(assert (= j (+ l z)))
(assert (= b (+ n w)))
(assert (= ah (+ o w)))
(assert (= e (/ t x)))
(assert (= aa (+ u ab)))
(assert (= g (/ v ac)))
(check-sat)
